COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00012 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.cb FISCAL YEAR 80 ACCOMPLISHMENTS AND FISCAL YEAR 81 PLANS

.CB FORMAL REASONING GROUP

.CB STANFORD ARTIFICIAL INTELLIGENCE LABORATORY

.CB Computer Science Department, Stanford University

	Professor John McCarthy continued his work on formalization
of common sense knowledge and common sense reasoning.  The goal is
to obtain a formal language for use by AI
programs with the precision of mathematical logic
and the expressiveness of natural language.

	McCarthy related his circumscription approach to non-monotonic
reasoning to the approaches of McDermott-Doyle and Reiter.  They cover
distinct AI requirements, but McCarthy's axiom schemata and circumscription
rule seem more suitable for computer use in both cases.

	McCarthy has a new approach to using first order logic
for expressing concepts that should be vaguely defined, because the
users of the concepts are referring to entities only a few of whose
properties they know.  This is related to recent work by philosophers
on "natural kinds".

	Thus a person hasn't a definition of lemon to which he is irrevocably
committed; we could accept blue lemons if there were good enough reasons
why they should be included, i.e. a person regards the concept of
a lemon as a natural kind existing outside himself and about whose
criteria he could learn more.  AI programs must use terms like
⊗bachelor whose definitions are conventional and natural kinds like
⊗lemon and treat them appropriately.  The technical consequence of
this common sense fact seems to be that the formal language doesn't
have a known preferred "standard model".

	During Fiscal 81, McCarthy will continue this research and
expects to prepare a paper on why AI programs need vague concepts
and how to make them work.  An AI memo will shortly be published
on McCarthy's Elephant formalism for proving facts about programs
in first order logic.


	Jussi Ketonen has been working on fragments of predicate calculus 
admitting fast decision procedures. Predicate logic has been traditionally 
viewed as the place to formalize the notion of a "logical inference";
intuitively it is clear that any "trivial" inference should be easily
formalizable and decidable in predicate logic. As is well known,
the full system of predicate calculus is not decidable; thus we one is led
to study suitable fragments of predicate logic. Ketonen has isolated a 
fragment that seems particularly promising: In some intuitive sense it 
captures the notion of a "direct" inference. The corresponding decision
procedure works in exponential time and is tailored to situations that
occur naturally in actual mathematical practice. 
This work will be described in detail in a forthcoming paper 
by Ketonen and Weyhrauch. Ketonen has written a program that implements the
above-mentioned decision procedure in the FOL proof checking program at SAIL.
The results were encouraging though somewhat inconclusive due 
to the technical difficulties encountered in the FOL environment.

	Ketonen is currently in the process of designing and implementing
a new mathematically oriented proof-checker in which to test the above 
mentioned ideas. The proposed proof-checker would be radically different 
from all its predecessors in its expressive power and its ability to 
manipulate proofs. For example, we can then implement procedures to 
unwind proofs of well known mathematical theorems, say, the 
recent non-constructive proofs of Van der Waerden's theorem. This kind
of a task is purely mechanical in character yet quite impossible to do
by hand. The interest in this endeavor lies in finding new upper
bounds for the numerical function occurring in Van der Waerden's theorem;
the previously known bounds are very bad.

	Ketonen hopes to have a small subset of his system running by the
end of the summer. The top level language has not been decided yet and 
will be the subject of intense thought.


   Lewis Creary continued his work on the epistemology of artificial
intelligence, and on the design of an advice-taking problem solver.

   On the epistemological side, new ideas were developed for dealing with:
 a) causal reasoning and the frame and qualification problems,
 b) the formal representation of actions,
 c) epistemic feasibility of actions and the need to plan for the
    availability of knowledge, and
 d) the structuring, classification, and use of domain-specific
    knowledge within a general problem solving system.

   Work on the advice-taking problem solver was concentrated for the most
part on high-level design issues and associated theoretical questions.
A tentative high-level design and long term plan were constructed,
incorporating the epistemological ideas mentioned above, as well as new
theoretical ideas concerning:
 e) problematic goal seeking, goal refinement, and achievement planning
 f) advice seeking and taking as a means of program development and selective
    knowledge acquisition,
 g) complex motivational structures for use in problem solving.

Also, work was begun on a detailed design for a modest initial implementation
of the problem solver as an advice-taking travel and communications planner.

During Fiscal 81, Creary plans to finish the initial detailed design of the
problem solver and to construct an experimental implementation of it as a
basis for further development.  He also expects to produce some papers
expounding the theoretical ideas on epistemology and on problem solving that
were developed during the past year.